<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Table of contents</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<script>

$(document).ready(function() {

    $("#accordion").show().accordion({
        autoHeight: false
    });

    $("#accordion div").css({ 'height': 'auto' });
});      


$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };
    
    $( "#accordion" ).accordion({
      icons: icons
    });
    $("#accordion").accordion({collapsible : true, active : 'none'});

    $( "#toggle" ).button().on( "click", function() {
      if ( $( "#accordion" ).accordion( "option", "icons" ) ) {
        $( "#accordion" ).accordion( "option", "icons", null );
      } else {
        $( "#accordion" ).accordion( "option", "icons", icons );
      }
    });
  } );
  </script>
<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: Programming Language Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</div>
</a></div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">Preface</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html">Top</a>
<li><a href="Preface.html#lab1">Welcome</a>

</li>
<li><a href="Preface.html#lab2">Overview</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab3">Program Verification</a>

</li>
<li><a href="Preface.html#lab4">Type Systems</a>

</li>
<li><a href="Preface.html#lab5">Further Reading</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab6">Note for Instructors</a>

</li>
<li><a href="Preface.html#lab7">Thanks</a>

</li>
</ul>
</div>
<h2><a href="Equiv.html">Program Equivalence&nbsp;&nbsp;&nbsp;&nbsp;(<i>Equiv</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Equiv.html">Top</a>
<li><a href="Equiv.html#lab9">Behavioral Equivalence</a>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab10">Definitions</a>

</li>
<li><a href="Equiv.html#lab11">Simple Examples</a>

</li>
</ul>
</div>

</li>
<li><a href="Equiv.html#lab21">Properties of Behavioral Equivalence</a>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab22">Behavioral Equivalence Is an Equivalence</a>

</li>
<li><a href="Equiv.html#lab23">Behavioral Equivalence Is a Congruence</a>

</li>
</ul>
</div>

</li>
<li><a href="Equiv.html#lab27">Program Transformations</a>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab28">The Constant-Folding Transformation</a>

</li>
<li><a href="Equiv.html#lab29">Soundness of Constant Folding</a>

</li>
</ul>
</div>

</li>
<li><a href="Equiv.html#lab34">Proving Inequivalence</a>

</li>
<li><a href="Equiv.html#lab37">Extended Exercise: Nondeterministic Imp</a>

</li>
<li><a href="Equiv.html#lab45">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Hoare.html">Hoare Logic, Part I&nbsp;&nbsp;&nbsp;&nbsp;(<i>Hoare</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Hoare.html">Top</a>
<li><a href="Hoare.html#lab49">Assertions</a>

</li>
<li><a href="Hoare.html#lab51">Hoare Triples</a>

</li>
<li><a href="Hoare.html#lab54">Proof Rules</a>
<div>
<ul class="doclist">
<li><a href="Hoare.html#lab55">Assignment</a>

</li>
<li><a href="Hoare.html#lab60">Consequence</a>

</li>
<li><a href="Hoare.html#lab61">Digression: The <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> Tactic</a>

</li>
<li><a href="Hoare.html#lab63">Skip</a>

</li>
<li><a href="Hoare.html#lab64">Sequencing</a>

</li>
<li><a href="Hoare.html#lab68">Conditionals</a>

</li>
<li><a href="Hoare.html#lab73">Loops</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare.html#lab76">Summary</a>

</li>
<li><a href="Hoare.html#lab77">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Hoare2.html">Hoare Logic, Part II&nbsp;&nbsp;&nbsp;&nbsp;(<i>Hoare2</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Hoare2.html">Top</a>
<li><a href="Hoare2.html#lab80">Decorated Programs</a>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab81">Example: Swapping Using Addition and Subtraction</a>

</li>
<li><a href="Hoare2.html#lab82">Example: Simple Conditionals</a>

</li>
<li><a href="Hoare2.html#lab84">Example: Reduce to Zero</a>

</li>
<li><a href="Hoare2.html#lab85">Example: Division</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare2.html#lab86">Finding Loop Invariants</a>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab87">Example: Slow Subtraction</a>

</li>
<li><a href="Hoare2.html#lab88">Exercise: Slow Assignment</a>

</li>
<li><a href="Hoare2.html#lab90">Exercise: Slow Addition</a>

</li>
<li><a href="Hoare2.html#lab92">Example: Parity</a>

</li>
<li><a href="Hoare2.html#lab94">Example: Finding Square Roots</a>

</li>
<li><a href="Hoare2.html#lab95">Example: Squaring</a>

</li>
<li><a href="Hoare2.html#lab96">Exercise: Factorial</a>

</li>
<li><a href="Hoare2.html#lab98">Exercise: Min</a>

</li>
<li><a href="Hoare2.html#lab101">Exercise: Power Series</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare2.html#lab103">Weakest Preconditions (Optional)</a>

</li>
<li><a href="Hoare2.html#lab108">Formal Decorated Programs (Advanced)</a>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab109">Syntax</a>

</li>
<li><a href="Hoare2.html#lab110">Extracting Verification Conditions</a>

</li>
<li><a href="Hoare2.html#lab111">Automation</a>

</li>
<li><a href="Hoare2.html#lab112">Examples</a>

</li>
<li><a href="Hoare2.html#lab121">Further Exercises</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="HoareAsLogic.html">Hoare Logic as a Logic&nbsp;&nbsp;&nbsp;&nbsp;(<i>HoareAsLogic</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="HoareAsLogic.html">Top</a>
<li><a href="HoareAsLogic.html#lab128">Definitions</a>

</li>
<li><a href="HoareAsLogic.html#lab129">Properties</a>

</li>
</ul>
</div>
<h2><a href="Smallstep.html">Small-step Operational Semantics&nbsp;&nbsp;&nbsp;&nbsp;(<i>Smallstep</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Smallstep.html">Top</a>
<li><a href="Smallstep.html#lab134">A Toy Language</a>

</li>
<li><a href="Smallstep.html#lab136">Relations</a>
<div>
<ul class="doclist">
<li><a href="Smallstep.html#lab137">Values</a>

</li>
<li><a href="Smallstep.html#lab139">Strong Progress and Normal Forms</a>

</li>
</ul>
</div>

</li>
<li><a href="Smallstep.html#lab149">Multi-Step Reduction</a>
<div>
<ul class="doclist">
<li><a href="Smallstep.html#lab150">Examples</a>

</li>
<li><a href="Smallstep.html#lab154">Normal Forms Again</a>

</li>
<li><a href="Smallstep.html#lab157">Equivalence of Big-Step and Small-Step</a>

</li>
<li><a href="Smallstep.html#lab162">Additional Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Smallstep.html#lab165">Small-Step Imp</a>

</li>
<li><a href="Smallstep.html#lab166">Concurrent Imp</a>

</li>
<li><a href="Smallstep.html#lab169">A Small-Step Stack Machine</a>

</li>
<li><a href="Smallstep.html#lab171">Aside: A <span class="inlinecode"><span class="id" type="var">normalize</span></span> Tactic</a>

</li>
</ul>
</div>
<h2><a href="Types.html">Type Systems&nbsp;&nbsp;&nbsp;&nbsp;(<i>Types</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Types.html">Top</a>
<li><a href="Types.html#lab174">Typed Arithmetic Expressions</a>
<div>
<ul class="doclist">
<li><a href="Types.html#lab175">Syntax</a>

</li>
<li><a href="Types.html#lab176">Operational Semantics</a>

</li>
<li><a href="Types.html#lab177">Normal Forms and Values</a>

</li>
<li><a href="Types.html#lab181">Typing</a>

</li>
<li><a href="Types.html#lab184">Progress</a>

</li>
<li><a href="Types.html#lab187">Type Preservation</a>

</li>
<li><a href="Types.html#lab191">Type Soundness</a>

</li>
<li><a href="Types.html#lab192">Additional Exercises</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Stlc.html">The Simply Typed Lambda-Calculus&nbsp;&nbsp;&nbsp;&nbsp;(<i>Stlc</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Stlc.html">Top</a>
<li><a href="Stlc.html#lab203">Overview</a>

</li>
<li><a href="Stlc.html#lab204">Syntax</a>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab205">Types</a>

</li>
<li><a href="Stlc.html#lab206">Terms</a>

</li>
</ul>
</div>

</li>
<li><a href="Stlc.html#lab207">Operational Semantics</a>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab208">Values</a>

</li>
<li><a href="Stlc.html#lab209">Substitution</a>

</li>
<li><a href="Stlc.html#lab211">Reduction</a>

</li>
<li><a href="Stlc.html#lab212">Examples</a>

</li>
</ul>
</div>

</li>
<li><a href="Stlc.html#lab214">Typing</a>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab215">Contexts</a>

</li>
<li><a href="Stlc.html#lab216">Typing Relation</a>

</li>
<li><a href="Stlc.html#lab217">Examples</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="StlcProp.html">Properties of STLC&nbsp;&nbsp;&nbsp;&nbsp;(<i>StlcProp</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="StlcProp.html">Top</a>
<li><a href="StlcProp.html#lab221">Canonical Forms</a>

</li>
<li><a href="StlcProp.html#lab222">Progress</a>

</li>
<li><a href="StlcProp.html#lab224">Preservation</a>
<div>
<ul class="doclist">
<li><a href="StlcProp.html#lab225">Free Occurrences</a>

</li>
<li><a href="StlcProp.html#lab227">Substitution</a>

</li>
<li><a href="StlcProp.html#lab229">Main Theorem</a>

</li>
</ul>
</div>

</li>
<li><a href="StlcProp.html#lab231">Type Soundness</a>

</li>
<li><a href="StlcProp.html#lab233">Uniqueness of Types</a>

</li>
<li><a href="StlcProp.html#lab235">Additional Exercises</a>
<div>
<ul class="doclist">
<li><a href="StlcProp.html#lab244">Exercise: STLC with Arithmetic</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="MoreStlc.html">More on the Simply Typed Lambda-Calculus&nbsp;&nbsp;&nbsp;&nbsp;(<i>MoreStlc</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="MoreStlc.html">Top</a>
<li><a href="MoreStlc.html#lab246">Simple Extensions to STLC</a>
<div>
<ul class="doclist">
<li><a href="MoreStlc.html#lab247">Numbers</a>

</li>
<li><a href="MoreStlc.html#lab248">Let Bindings</a>

</li>
<li><a href="MoreStlc.html#lab249">Pairs</a>

</li>
<li><a href="MoreStlc.html#lab250">Unit</a>

</li>
<li><a href="MoreStlc.html#lab251">Sums</a>

</li>
<li><a href="MoreStlc.html#lab252">Lists</a>

</li>
<li><a href="MoreStlc.html#lab253">General Recursion</a>

</li>
<li><a href="MoreStlc.html#lab256">Records</a>

</li>
</ul>
</div>

</li>
<li><a href="MoreStlc.html#lab259">Exercise: Formalizing the Extensions</a>
<div>
<ul class="doclist">
<li><a href="MoreStlc.html#lab265">Examples</a>

</li>
<li><a href="MoreStlc.html#lab274">Properties of Typing</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Sub.html">Subtyping&nbsp;&nbsp;&nbsp;&nbsp;(<i>Sub</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Sub.html">Top</a>
<li><a href="Sub.html#lab283">Concepts</a>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab284">A Motivating Example</a>

</li>
<li><a href="Sub.html#lab285">Subtyping and Object-Oriented Languages</a>

</li>
<li><a href="Sub.html#lab286">The Subsumption Rule</a>

</li>
<li><a href="Sub.html#lab287">The Subtype Relation</a>

</li>
<li><a href="Sub.html#lab295">Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Sub.html#lab309">Formal Definitions</a>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab310">Core Definitions</a>

</li>
<li><a href="Sub.html#lab314">Subtyping</a>

</li>
<li><a href="Sub.html#lab318">Typing</a>

</li>
</ul>
</div>

</li>
<li><a href="Sub.html#lab322">Properties</a>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab323">Inversion Lemmas for Subtyping</a>

</li>
<li><a href="Sub.html#lab326">Canonical Forms</a>

</li>
<li><a href="Sub.html#lab328">Progress</a>

</li>
<li><a href="Sub.html#lab329">Inversion Lemmas for Typing</a>

</li>
<li><a href="Sub.html#lab330">Context Invariance</a>

</li>
<li><a href="Sub.html#lab331">Substitution</a>

</li>
<li><a href="Sub.html#lab332">Preservation</a>

</li>
<li><a href="Sub.html#lab333">Records, via Products and Top</a>

</li>
<li><a href="Sub.html#lab334">Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Sub.html#lab336">Exercise: Adding Products</a>

</li>
</ul>
</div>
<h2><a href="Typechecking.html">A Typechecker for STLC&nbsp;&nbsp;&nbsp;&nbsp;(<i>Typechecking</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Typechecking.html">Top</a>
<li><a href="Typechecking.html#lab338">Comparing Types</a>

</li>
<li><a href="Typechecking.html#lab339">The Typechecker</a>

</li>
<li><a href="Typechecking.html#lab340">Digression: Improving the Notation</a>

</li>
<li><a href="Typechecking.html#lab341">Properties</a>

</li>
<li><a href="Typechecking.html#lab342">Exercises</a>

</li>
</ul>
</div>
<h2><a href="Records.html">Adding Records to STLC&nbsp;&nbsp;&nbsp;&nbsp;(<i>Records</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Records.html">Top</a>
<li><a href="Records.html#lab346">Adding Records</a>

</li>
<li><a href="Records.html#lab347">Formalizing Records</a>
<div>
<ul class="doclist">
<li><a href="Records.html#lab353">Examples</a>

</li>
<li><a href="Records.html#lab355">Properties of Typing</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="References.html">Typing Mutable References&nbsp;&nbsp;&nbsp;&nbsp;(<i>References</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="References.html">Top</a>
<li><a href="References.html#lab361">Definitions</a>

</li>
<li><a href="References.html#lab362">Syntax</a>

</li>
<li><a href="References.html#lab367">Pragmatics</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab368">Side Effects and Sequencing</a>

</li>
<li><a href="References.html#lab369">References and Aliasing</a>

</li>
<li><a href="References.html#lab370">Shared State</a>

</li>
<li><a href="References.html#lab371">Objects</a>

</li>
<li><a href="References.html#lab373">References to Compound Types</a>

</li>
<li><a href="References.html#lab375">Null References</a>

</li>
<li><a href="References.html#lab376">Garbage Collection</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab378">Operational Semantics</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab379">Locations</a>

</li>
<li><a href="References.html#lab380">Stores</a>

</li>
<li><a href="References.html#lab381">Reduction</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab382">Typing</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab383">Store typings</a>

</li>
<li><a href="References.html#lab385">The Typing Relation</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab386">Properties</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab387">Well-Typed Stores</a>

</li>
<li><a href="References.html#lab389">Extending Store Typings</a>

</li>
<li><a href="References.html#lab390">Preservation, Finally</a>

</li>
<li><a href="References.html#lab391">Substitution Lemma</a>

</li>
<li><a href="References.html#lab392">Assignment Preserves Store Typing</a>

</li>
<li><a href="References.html#lab393">Weakening for Stores</a>

</li>
<li><a href="References.html#lab394">Preservation!</a>

</li>
<li><a href="References.html#lab396">Progress</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab397">References and Nontermination</a>

</li>
<li><a href="References.html#lab399">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="RecordSub.html">Subtyping with Records&nbsp;&nbsp;&nbsp;&nbsp;(<i>RecordSub</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="RecordSub.html">Top</a>
<li><a href="RecordSub.html#lab401">Core Definitions</a>

</li>
<li><a href="RecordSub.html#lab406">Subtyping</a>
<div>
<ul class="doclist">
<li><a href="RecordSub.html#lab407">Definition</a>

</li>
<li><a href="RecordSub.html#lab408">Examples</a>

</li>
<li><a href="RecordSub.html#lab413">Properties of Subtyping</a>

</li>
</ul>
</div>

</li>
<li><a href="RecordSub.html#lab419">Typing</a>
<div>
<ul class="doclist">
<li><a href="RecordSub.html#lab420">Typing Examples</a>

</li>
<li><a href="RecordSub.html#lab424">Properties of Typing</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Norm.html">Normalization of STLC&nbsp;&nbsp;&nbsp;&nbsp;(<i>Norm</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Norm.html">Top</a>
<li><a href="Norm.html#lab434">Language</a>

</li>
<li><a href="Norm.html#lab442">Normalization</a>
<div>
<ul class="doclist">
<li><a href="Norm.html#lab443">Membership in <span class="inlinecode"><span class="id" type="var">R_T</span></span> Is Invariant Under Reduction</a>

</li>
<li><a href="Norm.html#lab444">Closed Instances of Terms of Type <span class="inlinecode"><span class="id" type="var">t</span></span> Belong to <span class="inlinecode"><span class="id" type="var">R_T</span></span></a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="LibTactics.html">A Collection of Handy General-Purpose Tactics&nbsp;&nbsp;&nbsp;&nbsp;(<i>LibTactics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="LibTactics.html">Top</a>
<li><a href="LibTactics.html#lab453">Tools for Programming with Ltac</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab454">Identity Continuation</a>

</li>
<li><a href="LibTactics.html#lab455">Untyped Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab456">Optional Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab457">Wildcard Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab458">Position Markers</a>

</li>
<li><a href="LibTactics.html#lab459">List of Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab460">Databases of Lemmas</a>

</li>
<li><a href="LibTactics.html#lab461">On-the-Fly Removal of Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab462">Numbers as Arguments</a>

</li>
<li><a href="LibTactics.html#lab463">Testing Tactics</a>

</li>
<li><a href="LibTactics.html#lab464">Testing evars and non-evars</a>

</li>
<li><a href="LibTactics.html#lab465">Check No Evar in Goal</a>

</li>
<li><a href="LibTactics.html#lab466">Helper Function for Introducing Evars</a>

</li>
<li><a href="LibTactics.html#lab467">Tagging of Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab468">More Tagging of Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab469">Deconstructing Terms</a>

</li>
<li><a href="LibTactics.html#lab470">Action at Occurence and Action Not at Occurence</a>

</li>
<li><a href="LibTactics.html#lab471">An Alias for <span class="inlinecode"><span class="id" type="var">eq</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab472">Common Tactics for Simplifying Goals Like <span class="inlinecode"><span class="id" type="tactic">intuition</span></span></a>

</li>
<li><a href="LibTactics.html#lab473">Backward and Forward Chaining</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab474">Application</a>

</li>
<li><a href="LibTactics.html#lab475">Assertions</a>

</li>
<li><a href="LibTactics.html#lab476">Instantiation and Forward-Chaining</a>

</li>
<li><a href="LibTactics.html#lab477">Experimental Tactics for Application</a>

</li>
<li><a href="LibTactics.html#lab478">Adding Assumptions</a>

</li>
<li><a href="LibTactics.html#lab479">Application of Tautologies</a>

</li>
<li><a href="LibTactics.html#lab480">Application Modulo Equalities</a>

</li>
<li><a href="LibTactics.html#lab481">Absurd Goals</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab482">Introduction and Generalization</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab483">Introduction</a>

</li>
<li><a href="LibTactics.html#lab484">Introduction using <span class="inlinecode">⇒</span> and <span class="inlinecode">=&gt;&gt;</span></a>

</li>
<li><a href="LibTactics.html#lab485">Generalization</a>

</li>
<li><a href="LibTactics.html#lab486">Naming</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab487">Rewriting</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab488">Replace</a>

</li>
<li><a href="LibTactics.html#lab489">Change</a>

</li>
<li><a href="LibTactics.html#lab490">Renaming</a>

</li>
<li><a href="LibTactics.html#lab491">Unfolding</a>

</li>
<li><a href="LibTactics.html#lab492">Simplification</a>

</li>
<li><a href="LibTactics.html#lab493">Reduction</a>

</li>
<li><a href="LibTactics.html#lab494">Substitution</a>

</li>
<li><a href="LibTactics.html#lab495">Tactics to Work with Proof Irrelevance</a>

</li>
<li><a href="LibTactics.html#lab496">Proving Equalities</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab497">Inversion</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab498">Basic Inversion</a>

</li>
<li><a href="LibTactics.html#lab499">Inversion with Substitution</a>

</li>
<li><a href="LibTactics.html#lab500">Injection with Substitution</a>

</li>
<li><a href="LibTactics.html#lab501">Inversion and Injection with Substitution &mdash;rough implementation</a>

</li>
<li><a href="LibTactics.html#lab502">Case Analysis</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab503">Induction</a>

</li>
<li><a href="LibTactics.html#lab504">Coinduction</a>

</li>
<li><a href="LibTactics.html#lab505">Decidable Equality</a>

</li>
<li><a href="LibTactics.html#lab506">Equivalence</a>

</li>
<li><a href="LibTactics.html#lab507">N-ary Conjunctions and Disjunctions</a>

</li>
<li><a href="LibTactics.html#lab508">Tactics to Prove Typeclass Instances</a>

</li>
<li><a href="LibTactics.html#lab509">Tactics to Invoke Automation</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab510">Definitions for Parsing Compatibility</a>

</li>
<li><a href="LibTactics.html#lab511"><span class="inlinecode"><span class="id" type="var">hint</span></span> to Add Hints Local to a Lemma</a>

</li>
<li><a href="LibTactics.html#lab512"><span class="inlinecode"><span class="id" type="var">jauto</span></span>, a New Automation Tactic</a>

</li>
<li><a href="LibTactics.html#lab513">Definitions of Automation Tactics</a>

</li>
<li><a href="LibTactics.html#lab514">Parsing for Light Automation</a>

</li>
<li><a href="LibTactics.html#lab515">Parsing for Strong Automation</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab516">Tactics to Sort Out the Proof Context</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab517">Hiding Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab518">Sorting Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab519">Clearing Hypotheses</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab520">Tactics for Development Purposes</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab521">Skipping Subgoals</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab522">Compatibility with standard library</a>

</li>
</ul>
</div>
<h2><a href="UseTactics.html">Tactic Library for Coq: A Gentle Introduction&nbsp;&nbsp;&nbsp;&nbsp;(<i>UseTactics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="UseTactics.html">Top</a>
<li><a href="UseTactics.html#lab523">Tactics for Naming and Performing Inversion</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab524">The Tactic <span class="inlinecode"><span class="id" type="var">introv</span></span></a>

</li>
<li><a href="UseTactics.html#lab525">The Tactic <span class="inlinecode"><span class="id" type="var">inverts</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab526">Tactics for N-ary Connectives</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab527">The Tactic <span class="inlinecode"><span class="id" type="var">splits</span></span></a>

</li>
<li><a href="UseTactics.html#lab528">The Tactic <span class="inlinecode"><span class="id" type="var">branch</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab529">Tactics for Working with Equality</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab530">The Tactics <span class="inlinecode"><span class="id" type="var">asserts_rewrite</span></span> and <span class="inlinecode"><span class="id" type="var">cuts_rewrite</span></span></a>

</li>
<li><a href="UseTactics.html#lab531">The Tactic <span class="inlinecode"><span class="id" type="var">substs</span></span></a>

</li>
<li><a href="UseTactics.html#lab532">The Tactic <span class="inlinecode"><span class="id" type="var">fequals</span></span></a>

</li>
<li><a href="UseTactics.html#lab533">The Tactic <span class="inlinecode"><span class="id" type="var">applys_eq</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab534">Some Convenient Shorthands</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab535">The Tactic <span class="inlinecode"><span class="id" type="var">unfolds</span></span></a>

</li>
<li><a href="UseTactics.html#lab536">The Tactics <span class="inlinecode"><span class="id" type="var">false</span></span> and <span class="inlinecode"><span class="id" type="var">tryfalse</span></span></a>

</li>
<li><a href="UseTactics.html#lab537">The Tactic <span class="inlinecode"><span class="id" type="var">gen</span></span></a>

</li>
<li><a href="UseTactics.html#lab538">The Tactics <span class="inlinecode"><span class="id" type="var">admits</span></span>, <span class="inlinecode"><span class="id" type="var">admit_rewrite</span></span> and <span class="inlinecode"><span class="id" type="var">admit_goal</span></span></a>

</li>
<li><a href="UseTactics.html#lab539">The Tactic <span class="inlinecode"><span class="id" type="var">sort</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab540">Tactics for Advanced Lemma Instantiation</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab541">Working of <span class="inlinecode"><span class="id" type="var">lets</span></span></a>

</li>
<li><a href="UseTactics.html#lab542">Working of <span class="inlinecode"><span class="id" type="var">applys</span></span>, <span class="inlinecode"><span class="id" type="var">forwards</span></span> and <span class="inlinecode"><span class="id" type="var">specializes</span></span></a>

</li>
<li><a href="UseTactics.html#lab543">Example of Instantiations</a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab544">Summary</a>

</li>
</ul>
</div>
<h2><a href="UseAuto.html">Theory and Practice of Automation in Coq Proofs&nbsp;&nbsp;&nbsp;&nbsp;(<i>UseAuto</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="UseAuto.html">Top</a>
<li><a href="UseAuto.html#lab545">Basic Features of Proof Search</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab546">Strength of Proof Search</a>

</li>
<li><a href="UseAuto.html#lab547">Basics</a>

</li>
<li><a href="UseAuto.html#lab548">Conjunctions</a>

</li>
<li><a href="UseAuto.html#lab549">Disjunctions</a>

</li>
<li><a href="UseAuto.html#lab550">Existentials</a>

</li>
<li><a href="UseAuto.html#lab551">Negation</a>

</li>
<li><a href="UseAuto.html#lab552">Equalities</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab553">How Proof Search Works</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab554">Search Depth</a>

</li>
<li><a href="UseAuto.html#lab555">Backtracking</a>

</li>
<li><a href="UseAuto.html#lab556">Adding Hints</a>

</li>
<li><a href="UseAuto.html#lab557">Integration of Automation in Tactics</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab558">Example Proofs using Automation</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab559">Determinism</a>

</li>
<li><a href="UseAuto.html#lab560">Preservation for STLC</a>

</li>
<li><a href="UseAuto.html#lab561">Progress for STLC</a>

</li>
<li><a href="UseAuto.html#lab562">BigStep and SmallStep</a>

</li>
<li><a href="UseAuto.html#lab563">Preservation for STLCRef</a>

</li>
<li><a href="UseAuto.html#lab564">Progress for STLCRef</a>

</li>
<li><a href="UseAuto.html#lab565">Subtyping</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab566">Advanced Topics in Proof Search</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab567">Stating Lemmas in the Right Way</a>

</li>
<li><a href="UseAuto.html#lab568">Unfolding of Definitions During Proof-Search</a>

</li>
<li><a href="UseAuto.html#lab569">Automation for Proving Absurd Goals</a>

</li>
<li><a href="UseAuto.html#lab570">Automation for Transitivity Lemmas</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab571">Decision Procedures</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab572">Omega</a>

</li>
<li><a href="UseAuto.html#lab573">Ring</a>

</li>
<li><a href="UseAuto.html#lab574">Congruence</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab575">Summary</a>

</li>
</ul>
</div>
<h2><a href="PE.html">Partial Evaluation&nbsp;&nbsp;&nbsp;&nbsp;(<i>PE</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="PE.html">Top</a>
<li><a href="PE.html#lab576">Generalizing Constant Folding</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab577">Partial States</a>

</li>
<li><a href="PE.html#lab578">Arithmetic Expressions</a>

</li>
<li><a href="PE.html#lab579">Boolean Expressions</a>

</li>
</ul>
</div>

</li>
<li><a href="PE.html#lab580">Partial Evaluation of Commands, Without Loops</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab581">Assignment</a>

</li>
<li><a href="PE.html#lab582">Conditional</a>

</li>
<li><a href="PE.html#lab583">The Partial Evaluation Relation</a>

</li>
<li><a href="PE.html#lab584">Examples</a>

</li>
<li><a href="PE.html#lab585">Correctness of Partial Evaluation</a>

</li>
</ul>
</div>

</li>
<li><a href="PE.html#lab586">Partial Evaluation of Loops</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab587">Examples</a>

</li>
<li><a href="PE.html#lab588">Correctness</a>

</li>
</ul>
</div>

</li>
<li><a href="PE.html#lab589">Partial Evaluation of Flowchart Programs</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab590">Basic blocks</a>

</li>
<li><a href="PE.html#lab591">Flowchart programs</a>

</li>
<li><a href="PE.html#lab592">Partial Evaluation of Basic Blocks and Flowchart Programs</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Postscript.html">Postscript</a></h2>
<div>
<ul class="doclist">
<li><a href="Postscript.html">Top</a>
<li><a href="Postscript.html#lab593">Looking Back</a>

</li>
<li><a href="Postscript.html#lab594">Looking Around</a>

</li>
<li><a href="Postscript.html#lab603">Looking Forward</a>

</li>
</ul>
</div>
<h2><a href="Bib.html">Bibliography&nbsp;&nbsp;&nbsp;&nbsp;(<i>Bib</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Bib.html">Top</a>
<li><a href="Bib.html#lab604">Resources cited in this volume</a>

</li>
</ul>
</div>
</div>
</div>

</div>

</div>
</body>
</html>